﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Pex.Framework;
using Microsoft.Pex.Framework.Goals;

namespace MicroBenchmarks.MultiClassNoSideEffects
{
    [PexClass(typeof(StepClass1))]
    public partial class MultiClassTest
    {
        /// <summary>
        /// A scenario where the desired object state is 
        /// </summary>
        /// <param name="sc1"></param>
        /// <param name="sc2"></param>
        [PexMethod]
        [PexAssertReachEventually]
        [PexMe.Attribute.FieldAccessObserver]
        [PexMe.Attribute.InsufficientObjectFactoryObserver]
        public void MultiClassTestPUT([PexAssumeNotNull]StepClass1 sc1, [PexAssumeNotNull]StepClass2 sc2)
        {
            if (sc1.Counter + sc2.Counter > 10)
                PexAssert.ReachEventually();
        }
    }
}
